es:event_system{i:l}, i,x:Id, ds:fpf(Id; x.Type), k:Knd, T:Type,
f:(decl-state(ds)Trationalsdecl-type{i:l}
f:(decl-state(ds)Trationalsdecl-type(ds; x)).
effect_p(es; i; ds; k; T; x; f)  prop{i:l} 

latex

Definitions	suptype(S; T), subtype(S; T), es-state(es; i), es_vartype(es; i; x), x. t(x), P  Q, P  Q, A c B, effect_p(es; i; ds; k; T; x; f), prop{i:l}, t  T, decl-type{i:l}(ds; x), decl-state(ds), Knd, fpf(A; a.B(a)), x:A. B(x), es_state(es; i), x(s), es-vartype(es; i; x)
Lemmas	event system wf, l member wf, IdLnk wf, rationals wf, decl-state wf, fpf-cap-void-subtype, es-val wf, subtype rel self, subtype rel dep function, es-state-when wf, top wf, id-deq wf, Id wf, fpf-cap wf, es-vartype wf, subtype rel function, es state wf, es state after wf, es-loc wf, alle-at wf